package bcontractor.propositional.minisat;

import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.IOException;

import org.apache.commons.io.IOUtils;

import bcontractor.api.SentenceSet;
import bcontractor.base.AbstractSATReasoner;
import bcontractor.propositional.PropositionalSentence;

/**
 * Resolvedor que delega o serviço para o MiniSat
 * 
 * @author lundberg
 * 
 */
public class MiniSatReasoner extends AbstractSATReasoner<PropositionalSentence> {

	private static final String MINISAT_PATH = "MINISAT_PATH";

	private static final String DEFAULT_MINISAT_PATH = "bin/minisat";

	private MiniSatOutputParser outputParser = new MiniSatOutputParser();

	@Override
	public boolean isSatisfiable(SentenceSet<PropositionalSentence> sentences) {
		try {
			File inputFile = File.createTempFile("problem", ".dimacs");
			this.prepareInputFile(sentences, inputFile);
			String command = this.getMiniSatPath() + " " + inputFile.getCanonicalPath();
			Process process = Runtime.getRuntime().exec(command);
			String output = IOUtils.toString(process.getInputStream());
			process.waitFor();
			process.destroy();
			inputFile.delete();
			MiniSatResult result = this.outputParser.parseOutput(output);
			return result.isSatisfiable();
		} catch (IOException e) {
			throw new RuntimeException("Erro de IO inesperado durante resolução do problema.", e);
		} catch (InterruptedException e) {
			throw new RuntimeException("Operação cancelada.", e);
		}
	}

	private String getMiniSatPath() {
		return System.getProperty(MINISAT_PATH, DEFAULT_MINISAT_PATH);
	}

	private void prepareInputFile(SentenceSet<PropositionalSentence> sentences, File inputFile) throws FileNotFoundException, IOException {
		MiniSatInput input = null;
		FileOutputStream output = null;
		try {
			input = new MiniSatInput(sentences);
			try {
				output = new FileOutputStream(inputFile);
				IOUtils.copy(input, output);
			} finally {
				IOUtils.closeQuietly(output);
			}
		} finally {
			IOUtils.closeQuietly(input);
		}
	}

}
